Search Results

Documents authored by Dybjer, Peter

Document
DOI: 10.4230/LIPIcs.TYPES.2022.13
Type Theory with Explicit Universe Polymorphism

Authors: Marc Bezem, Thierry Coquand, Peter Dybjer, and Martín Escardó

Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)

Abstract
The aim of this paper is to refine and extend proposals by Sozeau and Tabareau and by Voevodsky for universe polymorphism in type theory. In those systems judgments can depend on explicit constraints between universe levels. We here present a system where we also have products indexed by universe levels and by constraints. Our theory has judgments for internal universe levels, built up from level variables by a successor operation and a binary supremum operation, and also judgments for equality of universe levels.
Cite as

Marc Bezem, Thierry Coquand, Peter Dybjer, and Martín Escardó. Type Theory with Explicit Universe Polymorphism. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 13:1-13:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{bezem_et_al:LIPIcs.TYPES.2022.13,
  author =	{Bezem, Marc and Coquand, Thierry and Dybjer, Peter and Escard\'{o}, Mart{\'\i}n},
  title =	{{Type Theory with Explicit Universe Polymorphism}},
  booktitle =	{28th International Conference on Types for Proofs and Programs (TYPES 2022)},
  pages =	{13:1--13:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-285-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{269},
  editor =	{Kesner, Delia and P\'{e}drot, Pierre-Marie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.13},
  URN =		{urn:nbn:de:0030-drops-184564},
  doi =		{10.4230/LIPIcs.TYPES.2022.13},
  annote =	{Keywords: type theory, universes in type theory, universe polymorphism, level-indexed products, constraint-indexed products}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.TYPES.2018
LIPIcs, Volume 130, TYPES'18, Complete Volume

Authors: Peter Dybjer, José Espírito Santo, and Luís Pinto

Published in: LIPIcs, Volume 130, 24th International Conference on Types for Proofs and Programs (TYPES 2018)

Abstract
LIPIcs, Volume 130, TYPES'18, Complete Volume
Cite as

24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@Proceedings{dybjer_et_al:LIPIcs.TYPES.2018,
  title =	{{LIPIcs, Volume 130, TYPES'18, Complete Volume}},
  booktitle =	{24th International Conference on Types for Proofs and Programs (TYPES 2018)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-106-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{130},
  editor =	{Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018},
  URN =		{urn:nbn:de:0030-drops-114507},
  doi =		{10.4230/LIPIcs.TYPES.2018},
  annote =	{Keywords: Theory of computation,Type theory; Constructive mathematics; Logic and verification; Program verification, Software and its engineering}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.TYPES.2018.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Peter Dybjer, José Espírito Santo, and Luís Pinto

Published in: LIPIcs, Volume 130, 24th International Conference on Types for Proofs and Programs (TYPES 2018)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 0:i-0:x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{dybjer_et_al:LIPIcs.TYPES.2018.0,
  author =	{Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{24th International Conference on Types for Proofs and Programs (TYPES 2018)},
  pages =	{0:i--0:x},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-106-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{130},
  editor =	{Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.0},
  URN =		{urn:nbn:de:0030-drops-114045},
  doi =		{10.4230/LIPIcs.TYPES.2018.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.TLCA.2015.138
Undecidability of Equality in the Free Locally Cartesian Closed Category

Authors: Simon Castellan, Pierre Clairambault, and Peter Dybjer

Published in: LIPIcs, Volume 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)

Abstract
We show that a version of Martin-Löf type theory with extensional identity, a unit type N1, Sigma, Pi, and a base type is a free category with families (supporting these type formers) both in a 1- and a 2-categorical sense. It follows that the underlying category of contexts is a free locally cartesian closed category in a 2-categorical sense because of a previously proved biequivalence. We then show that equality in this category is undecidable by reducing it to the undecidability of convertibility in combinatory logic.
Cite as

Simon Castellan, Pierre Clairambault, and Peter Dybjer. Undecidability of Equality in the Free Locally Cartesian Closed Category. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 138-152, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{castellan_et_al:LIPIcs.TLCA.2015.138,
  author =	{Castellan, Simon and Clairambault, Pierre and Dybjer, Peter},
  title =	{{Undecidability of Equality in the Free Locally Cartesian Closed Category}},
  booktitle =	{13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
  pages =	{138--152},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-87-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{38},
  editor =	{Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.138},
  URN =		{urn:nbn:de:0030-drops-51602},
  doi =		{10.4230/LIPIcs.TLCA.2015.138},
  annote =	{Keywords: Extensional type theory, locally cartesian closed categories, undecidab- ility}
}
Document
DOI: 10.4230/DagSemRep.317
Dependent Type Theory meets Practical Programming (Dagstuhl Seminar 01341)

Authors: Gilles Barthe, Peter Dybjer, and Peter Thiemann

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Gilles Barthe, Peter Dybjer, and Peter Thiemann. Dependent Type Theory meets Practical Programming (Dagstuhl Seminar 01341). Dagstuhl Seminar Report 317, pp. 1-13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2002)

Copy BibTex To Clipboard

@TechReport{barthe_et_al:DagSemRep.317,
  author =	{Barthe, Gilles and Dybjer, Peter and Thiemann, Peter},
  title =	{{Dependent Type Theory meets Practical Programming (Dagstuhl Seminar 01341)}},
  pages =	{1--13},
  ISSN =	{1619-0203},
  year =	{2002},
  type = 	{Dagstuhl Seminar Report},
  number =	{317},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemRep.317},
  URN =		{urn:nbn:de:0030-drops-152017},
  doi =		{10.4230/DagSemRep.317},
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact